YES 0.45 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/FiniteMap.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule FiniteMap
  ((isEmptyFM :: FiniteMap b a  ->  Bool) :: FiniteMap b a  ->  Bool)

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a


  instance (Eq a, Eq b) => Eq (FiniteMap b a) where 

  isEmptyFM :: FiniteMap a b  ->  Bool
isEmptyFM fm sizeFM fm == 0

  sizeFM :: FiniteMap b a  ->  Int
sizeFM EmptyFM 0
sizeFM (Branch _ _ size _ _) size


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule FiniteMap
  ((isEmptyFM :: FiniteMap a b  ->  Bool) :: FiniteMap a b  ->  Bool)

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a


  instance (Eq a, Eq b) => Eq (FiniteMap b a) where 

  isEmptyFM :: FiniteMap b a  ->  Bool
isEmptyFM fm sizeFM fm == 0

  sizeFM :: FiniteMap b a  ->  Int
sizeFM EmptyFM 0
sizeFM (Branch vw vx size vy vzsize


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ NumRed

mainModule FiniteMap
  ((isEmptyFM :: FiniteMap a b  ->  Bool) :: FiniteMap a b  ->  Bool)

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap a b = EmptyFM  | Branch a b Int (FiniteMap a b) (FiniteMap a b


  instance (Eq a, Eq b) => Eq (FiniteMap a b) where 

  isEmptyFM :: FiniteMap a b  ->  Bool
isEmptyFM fm sizeFM fm == 0

  sizeFM :: FiniteMap a b  ->  Int
sizeFM EmptyFM 0
sizeFM (Branch vw vx size vy vzsize


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ NumRed
HASKELL
              ↳ Narrow

mainModule FiniteMap
  (isEmptyFM :: FiniteMap a b  ->  Bool)

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap a b = EmptyFM  | Branch a b Int (FiniteMap a b) (FiniteMap a b


  instance (Eq a, Eq b) => Eq (FiniteMap b a) where 

  isEmptyFM :: FiniteMap a b  ->  Bool
isEmptyFM fm sizeFM fm == Pos Zero

  sizeFM :: FiniteMap a b  ->  Int
sizeFM EmptyFM Pos Zero
sizeFM (Branch vw vx size vy vzsize


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Haskell To QDPs